;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "Irng.lisp")
(require "Mrng.lisp")

(module Trng
  (import Irng)
  
  (include-book "testing" :dir :teachpacks)
  
  ; Test when seed is 0
  (check-expect (get-random-number 0) 12345)
  
  ; Test when seed is -1
  (check-expect (get-random-number -1) 3191464396)
  
  ; Test when seed is typical
  (check-expect (get-random-number 1234) 233191843)
  ; Follow up test to make sure next seed is correct
  (check-expect (get-random-number (get-random-number 1234)) 128476320)
  
  ; Test to check when seed is 0 and max is 1
  (check-expect (get-random-number-mod-max 0 1) (cons 0 12345))
  ; Test to check when seed is 0 and max is 2
  (check-expect (get-random-number-mod-max 0 2) (cons 1 12345))
  
  ; Test to check typical call, seed is 1234, max is 10
  (check-expect (get-random-number-mod-max 1234 10) (cons 3 233191843))
  ; Follow up to test to make sure next seed/return value is correct
  (check-expect (get-random-number-mod-max (get-random-number 1234) 10) (cons 0 128476320))
  
  (include-book "doublecheck" :dir :teachpacks)
  
  ; The RNG should never (reasonably) repeat
  (defproperty rng-doesnt-repeat
    (x :value (random-integer)
       :where (> x 0))
    (not (equal (get-random-number x) (get-random-number (get-random-number x))))
  )
  
  ; The RNG should not return a negative number
  (defproperty rng-not-negative
    (x :value (random-integer)
       :where (> x 0))
    (>= (get-random-number x) 0)
  )

  ; The RNG should return a number less than the maximum value given
  (defproperty rng-mod-max-less-than-max
    (x :value (random-integer)
     y :value (random-integer)
       :where (and (> x 0) (> y 0)))
    (< (car (get-random-number-mod-max x y)) y)
  )
  
  ; The RNG should not return a negative number less than the maximum value given
  (defproperty rng-mod-max-not-negative
    (x :value (random-integer)
     y :value (random-integer)
       :where (and (> x 0) (> y 0)))
    (>= (car (get-random-number-mod-max x y)) 0)
  )
)

(link RTrng (Mrng Trng))
(invoke RTrng)